00100	(LE(ADD1(J) X1) ∧ LE(X1 SUB1(CN))) → LE(A(X1) A(ADD1(X1)));
00200	(LE(U X1) ∧ LE( X1 SUB1(I)) ∧ LE(SUB1(I) CN))→ LE(A(X1) BIG);
00300	(LE(U X1) ∧ LE(X1 J) ∧ LE(J SUB1 (CN))) → LE(A(X1) A(ADD1(J)));
00400	E(BIG A(LOC));
00500	LE(U LOC) ∧ LE(LOC J) ;
00600	LE(ADD1 (U) I);
00700	E(LOC J);
00800	LE(ADD1(J) I);
00900	LE(ADD1 (U) J) ∧ LE(J CN);
01000	;
01100	
     

00100	
00200	∀(X1 X2 X3 X4)(((((LE(ADD1(X2) X1) ∧ LE(X1 X3))→LE(A(X1) A(ADD1(X1)))) ∧ LE(X2 X3)) →LE(A(X2) A(ADD1(X2))))
00300	  → ((LE(X2 X4) ∧ LE(X4 X3) )→ LE(A(X4) A(ADD1(X4)))));
00500	
     

00100	LE(X1 X2) ∨ LE(X2 X1);
00200	(LE(X1 X2) ∧ LE(X2 X1))→ E(X1 X2);
00300	(LE(X1 X2) ∧ LE(X2 X3)) → LE(X1 X3);
00400	LE(X1 ADD1(X1));
00500	¬E(X1 ADD1(X1));
00600	LE(X2 X1) ∨ LE(ADD1(X1) X2);
00700	LE(X1 X1);
00800	;
     

00100	∀(X1)((LE(J X1) ∧ LE(X1 SUB1 (CN))) → LE(A(X1) A(ADD1(X1))));
00200	;